/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model;

import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.strategy.GameStrategy;
import chameleon.model.NuGatStructure.strategy.StructCheckLTLGameSF07;
import chameleon.model.game.transition.Automata;
import chameleon.model.game.transition.Ltl;
import chameleon.model.game.*;
import java.io.File;
import java.io.IOException;

import org.xml.sax.SAXException;



/**
 * This class build the game structure. The game structure is a set of some
 * decorator object. For add a new decoration just do game.addDecoration(tag).
 *
 * So to create a new decorator, just declare new class extends GameDecorator,
 * add the corresponding tag in @model.game.Tag.java and add the corresponding
 * getter in @model.game.Game.java.
 *
 *
 * @author simon
 */
public class GameFactory {

    //*********************** CREATION METHOD *****************************//

    //construction with a smv file
    public static Game createGame (File model) throws IOException{
        Game game = new Game();

        game = addSmv(game, model);
        
        return game;
    }
    
    /**
     * Creation of a game wihout any input file.
     * @param player1
     * @param player
     * @return 
     */
    public static Game createGame(Player player1, Player player2){
        return null;
    }

    /**
     * Not used anymore!
     * 
     * This function convert an automaton to a BDD structure.
     * 
     * @param game
     * @param player
     * @return
     * @throws IOException
     * @throws SAXException
     */

    private static Game createBddForNBW(Game game, int player) throws IOException, SAXException {

        /*int tag = getTransTag(player);
        BddDecoration bdd;
        if (player == 1)
            bdd = new BddDecoration();
        else
            bdd = game.getBDD();
        int bitNbre;

        /** Before start the conversion we must to convert all our allTransition
         * relation to a NBW
         */

        /*TransitionRelation transition = game.getTransition(tag);
        transition.convert2NBW();

        
        /** First step : count the number of nodes presents in the automata
         * and store the node's name. 
         */
        /*DOMParser parser = new DOMParser();
        parser.parse(game.getTransition(tag).getFile().getPath());
        Document document = parser.getDocument();

        Element automata = document.getDocumentElement();
        NodeList nodeList = automata.getElementsByTagName("State");

        //In nodeList we have all the xml structure for nodes
        bitNbre = getBitNbre(nodeList.getLength());
        System.out.println("bitnbre : "+bitNbre);
        bdd.setNbreBitNode(bitNbre, player);

        //Compute the number of bit for the alphabet
        int alphaSize = game.getIAlphabet().getSize() + game.getOALphabet().getSize()+1;
        //+1 = true ;
        bdd.setNbreByteAlphabet(alphaSize);

        //store the nodes
        for (int i = 0; i < nodeList.getLength(); ++i)
            bdd.addNode(i, getBit(i,bitNbre),player);

        //strore the alphabet
        Vector<String> alphabet = game.getAlphabet();
        for (int i=0; i < alphabet.size(); ++i){
            bdd.addAtomicProposition(alphabet.get(i), i);
        }
        
        /**
         * Second step : analyze the tranition and create the boolean formula
         * that represents the allTransition function
         */

        /*NodeList from = automata.getElementsByTagName("From");
        NodeList to = automata.getElementsByTagName("To");
        NodeList label = automata.getElementsByTagName("Label");
        int dec = nodeList.getLength();
        Vector<Boolean[]> allTransition = new Vector<Boolean[]>();

        for (int i=0; i<from.getLength(); ++i){
            Integer name = Integer.parseInt(from.item(i).getFirstChild().getNodeValue());
            boolean[] source = bdd.getNode(name.intValue(),player);
            name = Integer.parseInt(to.item(i).getFirstChild().getNodeValue());
            boolean[] target = bdd.getNode(name.intValue(),player);

            boolean[] atomicProp = getLabel(label.item(i+dec).getFirstChild().getNodeValue(),
                    alphaSize,bdd,game);
            int size = source.length+target.length+atomicProp.length;

            bdd.setSizeBooleanFormula(size, player);

            Boolean[] trans = new Boolean[size];
            
            int sizeSource = source.length;
            int sizeAtomic = atomicProp.length;

            //The structure in NuGat is : prop : source destination

            //add source to trans
            for (int j = 0; j < source.length; ++j)
                trans[j] = source[j];
            //displayBool(source);

            //add label to trans
            for (int j=0; j < sizeAtomic; ++j)
                trans[j+sizeSource] = atomicProp[j];
            //displayBool(atomicProp);
            //add target to trans
            for (int j=0; j < target.length; ++j)
                trans[j+sizeSource+sizeAtomic] = target[j];
            //displayBool(target);
            System.out.println();
            allTransition.add(trans.clone());

            
        }
        if (player==1){
                bdd.addTrans(1, allTransition);
                bdd.createBDD(1);
            }
            else {
                bdd.addTrans(2, allTransition);
                bdd.createBDD(2);
            }
        
        game.addDecoration(bdd);
        return game;*/
        return null;
    }

    /**
     * Add an input smv file to the game structure.
     * 
     * @param game
     * @param file
     * @return
     */

    private static Game addSmv(Game game,File file){
        SmvFile smvFile = new SmvFile(file);
        game.addDecoration(smvFile);
        return game;
    }
    
    public static Game addGameBddFsm(Game game, GameBddFsm gameBddFsm){
        GameBddFsmDecorator dec = 
               new GameBddFsmDecorator(gameBddFsm);
       game.addDecoration(dec);
       return game; 
    }
    
    public static Game addStrategy (Game game, GameStrategy strategy){
        StrategyDecorator decoration = new StrategyDecorator(strategy);
        game.addDecoration(decoration);
        return game;
    }
    
    public static Game addNuGatInterface(Game game, NuGatInterface nugat){
        game.setNuGatInterface(nugat);
        return game;
    }
    
    /**
     * Add a save of the initial strategy
     * @param game
     * @param strategy
     * @return 
     */
    
    public static Game addInitStrategy(Game game, GameStrategy strategy){
        StrategyDecorator decoration = new StrategyDecorator(strategy);
        game.addDecoration(decoration, Tag.INIT_STRATEGY);
        return game;
    }

    public static Game addCls(Game game, StructCheckLTLGameSF07 cls){
        ClsDecorator decoration = new ClsDecorator(cls);
        game.addDecoration(decoration);
        return game;
    }
    
    /**
     * Add to the game structure a representation of some transition for one
     * player. This description can be an LTL formula or an automaton.
     *
     * @param game
     * @param trans
     * @param type
     * @param player
     * @return
     * @throws IOException
     */

    public static Game addTrans (Game game, File trans, int type, int player) throws IOException{
        if (type == Tag.AUTOMATA)
            game.addDecoration(createAutomata(trans, player),Tag.TRANSITION);
        else if (type == Tag.LTL)
            game.addDecoration(createLtl(trans, player),Tag.TRANSITION);
        else
            throw new IOException("GameFactory::Uncorrect kind of transition relation");
        return game;
    }

    /**
     * Create the automata decoration to game structure.
     * 
     * @param file
     * @param player
     * @return
     */

    private static Automata createAutomata (File file, int player){
        return new Automata(file,player);
    }

    /**
     * Create the LTL decoration to game structure.
     *
     * @param file
     * @param player
     * @return
     */

    private static Ltl createLtl(File file, int player){
        return new Ltl(file,player);
    }

    public static Game deleteStrategy(Game game){
        game.deleteDecoration(Tag.STRATEGY);
        return game;
    }
    
    /*private boolean[] getBit(int n, int sizeVec){
        int size;
        if (n !=0)
            size = ((int)Math.floor((Math.log(n))/Math.log(2)))+1;
        else
            size = 1;

        boolean[] bit = new boolean[sizeVec];
        //init bit to 0
        for (int i=1; i < sizeVec; ++i){
            bit[i] = false;
        }


        boolean finish = false;

        for (int i=0; i < size-1 && !finish; ++i){
            int div = n/2;
            boolean rest = (n%2) == 1 ;
            n = div;
            bit[sizeVec-i-1] = rest;
        }

        int pos = sizeVec-size;
        if (n == 1)
            bit[pos]=true;
        else
            bit[pos]=false;
        return bit;
    }*/

    /*private boolean[] getLabel(String str, int size, BddDecoration bdd, Game game) throws IOException {
        char[] label = str.toCharArray();
        boolean[] atomicProp = new boolean[size];
        isPlayer1_ = false;
        isPlayer2_ = false;

        //init atomicProp to 0
        for (int i=0; i<size; ++i )
            atomicProp[i] = false;


        boolean isTrue = true;
        String prop="";

        for (int i = 0; i < label.length; ++i){
            if (label[i] == '~')
                isTrue = false;
            else if (!Character.isWhitespace(label[i]))
                prop+=label[i];
            else{
                int pos = bdd.getAtomicProposition(prop);
                atomicProp[pos] = isTrue;
                if(!isPlayer1_ && isTrue)
                    isPlayer1_ = game.getIAlphabet().isInAlphabet(prop);
                if(!isPlayer2_ && isTrue)
                    isPlayer2_ = game.getOALphabet().isInAlphabet(prop);
                prop="";
                isTrue=true;
            }
        }
        int pos = bdd.getAtomicProposition(prop);
        atomicProp[pos] = isTrue;
        prop="";
        isTrue=true;
        return atomicProp;
    }*/

    /*private int getTransTag(int player) {
        if (player == 1)
            return Tag.TRANS_P1;
        else
            return Tag.TRANS_P2;
    }

    private int getBitNbre(int length) {
         if (length%2 == 0)
            return ((int)Math.floor((Math.log(length))/Math.log(2)));
        else
            return ((int)Math.floor((Math.log(length))/Math.log(2))+1);
    }*/

}
